\begin{tabbing}
$\vdash$  \=$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).\+
\\[0ex]($\forall$$x$, $y$:$T$. Dec($R$($x$,$y$)))
\\[0ex]$\Rightarrow$ Linorder($T$;$x$,$y$.$R$($x$,$y$))
\\[0ex]$\Rightarrow$ ($\forall$$a$, $b$:$T$. ($\neg$strict\_part($x$,$y$.$R$($x$,$y$);$a$;$b$)) $\Leftarrow\!\Rightarrow$ $R$($b$,$a$))
\-
\end{tabbing}